/*
 * Bogor: An Extensible and Highly-Modular Model Checking Framework Copyright
 * (c) 2002-2004 Kansas State University This software is licensed using the
 * SAnToS Laboratory Open Academic License. You should have received a copy of
 * the License in the top directory of this software distribution package. If
 * not, then write to SAnToS Laboratory, 234 Nichols Hall, Manhattan, KS 66506,
 * USA. The SAnToS Laboratory homepage is located at
 * http://www.cis.ksu.edu/santos. The Bogor homepage is located at
 * http://bogor.projects.cis.ksu.edu.
 */
package edu.ksu.cis.projects.bogor.ext.java;

import static edu.ksu.cis.projects.bogor.ext.java.LockingReductionConfigurationConstants.ATOMIC_METHOD_ID;
import static edu.ksu.cis.projects.bogor.ext.java.LockingReductionConfigurationConstants.COMM_RECORD_ID;
import static edu.ksu.cis.projects.bogor.ext.java.LockingReductionConfigurationConstants.GENERIC_LOCKING_ANNOTATIONS_PROPERTY_PREFIX;
import static edu.ksu.cis.projects.bogor.ext.java.LockingReductionConfigurationConstants.INVISIBLE_LOC_ID;
import static edu.ksu.cis.projects.bogor.ext.java.LockingReductionConfigurationConstants.LOCKING_RECORD_ID;
import static edu.ksu.cis.projects.bogor.ext.java.LockingReductionConfigurationConstants.LOCK_OPT_ID;
import static edu.ksu.cis.projects.bogor.ext.java.LockingReductionConfigurationConstants.READ_ONLY_FIELD_ID;
import static edu.ksu.cis.projects.bogor.ext.java.LockingReductionConfigurationConstants.READ_ONLY_FIELD_SEP_ID;
import static edu.ksu.cis.projects.bogor.ext.java.LockingReductionConfigurationConstants.READ_ONLY_INIT_ID;
import static edu.ksu.cis.projects.bogor.ext.java.LockingReductionConfigurationConstants.READ_ONLY_INIT_SEP_ID;
import static edu.ksu.cis.projects.bogor.ext.java.LockingReductionConfigurationConstants.UNSH_RECORD_ID;
import static edu.ksu.cis.projects.bogor.ext.java.LockingReductionConfigurationConstants.VISIBLE_LOC_ID;

import java.io.PrintWriter;
import java.io.StringWriter;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.List;
import java.util.ListIterator;
import java.util.Map;
import java.util.Properties;
import java.util.Set;
import java.util.StringTokenizer;

import edu.ksu.cis.projects.bogor.IBogorConfiguration;
import edu.ksu.cis.projects.bogor.ast.Action;
import edu.ksu.cis.projects.bogor.ast.AssignAction;
import edu.ksu.cis.projects.bogor.ast.BlockTransformation;
import edu.ksu.cis.projects.bogor.ast.Dependency;
import edu.ksu.cis.projects.bogor.ast.Exp;
import edu.ksu.cis.projects.bogor.ast.FSM;
import edu.ksu.cis.projects.bogor.ast.InvokeTransformation;
import edu.ksu.cis.projects.bogor.ast.Location;
import edu.ksu.cis.projects.bogor.ast.LocationInfo;
import edu.ksu.cis.projects.bogor.ast.NewArrayExp;
import edu.ksu.cis.projects.bogor.ast.NewRecordExp;
import edu.ksu.cis.projects.bogor.ast.Transformation;
import edu.ksu.cis.projects.bogor.module.ConfigurationMessages;
import edu.ksu.cis.projects.bogor.module.DefaultMessageStore;
import edu.ksu.cis.projects.bogor.module.IEnabledTransformationsContext;
import edu.ksu.cis.projects.bogor.module.IMessageStore;
import edu.ksu.cis.projects.bogor.module.ISchedulingStrategyContext;
import edu.ksu.cis.projects.bogor.module.ISchedulingStrategyInfo;
import edu.ksu.cis.projects.bogor.module.IStoreStateResult;
import edu.ksu.cis.projects.bogor.module.backtrack.IActionBacktrackingInfo;
import edu.ksu.cis.projects.bogor.module.backtrack.IFieldBacktrackingInfo;
import edu.ksu.cis.projects.bogor.module.backtrack.IGlobalBacktrackingInfo;
import edu.ksu.cis.projects.bogor.module.backtrack.ILocalBacktrackingInfo;
import edu.ksu.cis.projects.bogor.module.backtrack.INextStateBacktrackingInfo;
import edu.ksu.cis.projects.bogor.module.backtrack.IPostNextStateBacktrackingInfo;
import edu.ksu.cis.projects.bogor.module.backtrack.ITransformationBacktrackingInfo;
import edu.ksu.cis.projects.bogor.module.state.IState;
import edu.ksu.cis.projects.bogor.module.state.StateValueVisitor;
import edu.ksu.cis.projects.bogor.module.value.IArrayValue;
import edu.ksu.cis.projects.bogor.module.value.ILockValue;
import edu.ksu.cis.projects.bogor.module.value.INonPrimitiveValue;
import edu.ksu.cis.projects.bogor.module.value.IRecordValue;
import edu.ksu.cis.projects.bogor.module.value.IValue;
import edu.ksu.cis.projects.bogor.module.value.IValueVisitorAction;
import edu.ksu.cis.projects.bogor.module.value.ValueVisitor;
import edu.ksu.cis.projects.bogor.symboltable.FSMSymbolTable;
import edu.ksu.cis.projects.bogor.type.ArrayType;
import edu.ksu.cis.projects.bogor.type.PrimitiveExtType;
import edu.ksu.cis.projects.bogor.type.PrimitiveType;
import edu.ksu.cis.projects.bogor.type.RecordType;
import edu.ksu.cis.projects.bogor.type.Type;
import edu.ksu.cis.projects.bogor.util.FileMessage;
import edu.ksu.cis.projects.bogor.util.Pair;
import edu.ksu.cis.projects.bogor.util.Util;
import edu.ksu.cis.projects.trove.custom.IReadableIntObjectTable;
import edu.ksu.cis.projects.trove.custom.IntIntTable;
import edu.ksu.cis.projects.trove.custom.IntObjectTable;
import edu.ksu.cis.projects.trove.custom.IntSet;
import edu.ksu.cis.projects.trove.custom.ObjectIntTable;

/**
 * @author <a href="robby@cis.ksu.edu">Robby </a>
 * @version CVS $Revision: 1.40 $ $Date: 2005/11/03 17:50:53 $
 */
public class JavaSearcher
    extends PartialOrderingSearcher
{
    // ~ Static variables/initializers
    // ..........................................

    // ..........................................
    protected static final String GLOBAL_ISI = "isi";

    protected static final String RUN_STATIC_INITIALIZERS_ID = "runStaticInitializers";

    protected static final String USE_POR_ID = "usePOR";

    // ~ Instance variables
    // .....................................................
    // .....................................................
    protected ArrayList<String> lockingRecordNames;

    protected ArrayList<String> unshRecordNames;

    protected ArrayList<String> commRecordNames;

    protected ArrayList<Pair<String, Integer>> unshArrayNames;

    protected ArrayList<Pair<String, Integer>> commArrayNames;

    protected ArrayList<String> readOnlyFields;

    protected ArrayList<String> readOnlyInits;

    protected HashSet<String> atomicMethods;

    protected HashSet<String> invisibleLocIds;

    protected HashSet<String> visibleLocIds;

    protected IntSet lockingRecordTypeIds;

    protected IntSet unshRecordTypeIds;

    protected IntSet commRecordTypeIds;

    protected IntObjectTable<IntSet> readOnlyFieldTable;

    protected IntObjectTable<Set<String>> readOnlyInitTable;

    protected IntSet invisibleLocDescs;

    protected IntSet visibleLocDescs;

    protected String readOnlyFieldSep = "~";

    protected String readOnlyInitSep = "~";

    protected HashMap<IValue, Set<ILockValue>> lockSetMap;

    protected IntIntTable typeIdToPrivateLockIndexMap;

    protected IntSet violatingLDTypeIds;

    protected boolean lockOpt = true;

    protected boolean usePOR;

    protected int globalISIIndex;

    protected HashSet<String> warnings = new HashSet<String>();

    // ~ Methods
    // ................................................................

    @Override
    public IMessageStore setOptions(String key, Properties configuration)
    {
        String genericKey = GENERIC_LOCKING_ANNOTATIONS_PROPERTY_PREFIX;

        IMessageStore parentResult = super.setOptions(key, configuration);
        List<FileMessage> errors = parentResult.getErrors();
        List<FileMessage> warnings = parentResult.getWarnings();

        final String KEYED_LOCKING_RECORD_ID = key + "." + LOCKING_RECORD_ID
                                               + ".";
        final String GENERIC_LOCKING_RECORD_ID = genericKey + "."
                                                 + LOCKING_RECORD_ID + ".";

        final String KEYED_UNSH_RECORD_ID = key + "." + UNSH_RECORD_ID + ".";
        final String GENERIC_UNSH_RECORD_ID = genericKey + "." + UNSH_RECORD_ID
                                              + ".";

        final String KEYED_COMM_RECORD_ID = key + "." + COMM_RECORD_ID + ".";
        final String GENERIC_COMM_RECORD_ID = genericKey + "." + COMM_RECORD_ID
                                              + ".";

        final String KEYED_LOCK_OPT_ID = key + "." + LOCK_OPT_ID;
        final String GENERIC_LOCK_OPT_ID = genericKey + "." + LOCK_OPT_ID;

        final String KEYED_READ_ONLY_FIELD_ID = key + "." + READ_ONLY_FIELD_ID
                                                + ".";
        final String GENERIC_READ_ONLY_FIELD_ID = genericKey + "."
                                                  + READ_ONLY_FIELD_ID + ".";

        final String KEYED_READ_ONLY_INIT_ID = key + "." + READ_ONLY_INIT_ID
                                               + ".";
        final String GENERIC_READ_ONLY_INIT_ID = genericKey + "."
                                                 + READ_ONLY_INIT_ID + ".";

        final String KEYED_READ_ONLY_FIELD_SEP_ID = key + "."
                                                    + READ_ONLY_FIELD_SEP_ID;
        final String GENERIC_READ_ONLY_FIELD_SEP_ID = genericKey + "."
                                                      + READ_ONLY_FIELD_SEP_ID;

        final String KEYED_READ_ONLY_INIT_SEP_ID = key + "."
                                                   + READ_ONLY_INIT_SEP_ID;
        final String GENERIC_READ_ONLY_INIT_SEP_ID = genericKey + "."
                                                     + READ_ONLY_INIT_SEP_ID;

        final String KEYED_VISIBLE_LOC_ID = key + "." + VISIBLE_LOC_ID + ".";
        final String GENERIC_VISIBLE_LOC_ID = genericKey + "." + VISIBLE_LOC_ID
                                              + ".";

        final String KEYED_INVISIBLE_LOC_ID = key + "." + INVISIBLE_LOC_ID
                                              + ".";
        final String GENERIC_INVISIBLE_LOC_ID = genericKey + "."
                                                + INVISIBLE_LOC_ID + ".";

        final String KEYED_ATOMIC_METHOD_ID = key + "." + ATOMIC_METHOD_ID
                                              + ".";
        final String GENERIC_ATOMIC_METHOD_ID = genericKey + "."
                                                + ATOMIC_METHOD_ID + ".";

        final String USE_POR_ID = key + "." + JavaSearcher.USE_POR_ID;

        unshRecordNames = new ArrayList<String>();
        commRecordNames = new ArrayList<String>();
        unshArrayNames = new ArrayList<Pair<String, Integer>>();
        commArrayNames = new ArrayList<Pair<String, Integer>>();
        lockingRecordNames = new ArrayList<String>();
        readOnlyFields = new ArrayList<String>();
        readOnlyInits = new ArrayList<String>();
        invisibleLocIds = new HashSet<String>();
        visibleLocIds = new HashSet<String>();
        atomicMethods = new HashSet<String>();

        for (Iterator i = configuration.keySet().iterator(); i.hasNext();)
        {
            String optionId = (String) i.next();
            String value = configuration.getProperty(optionId).trim();

            if (optionId.startsWith(KEYED_UNSH_RECORD_ID)
                || optionId.startsWith(GENERIC_UNSH_RECORD_ID))
            {
                if (value.endsWith("[]"))
                {
                    int rank = 0;
                    while (value.endsWith("[]"))
                    {
                        rank++;
                        value = value.substring(0, value.length() - 2).trim();
                    }
                    unshArrayNames.add(new Pair<String, Integer>(value, rank));
                }
                else
                {
                    unshRecordNames.add(value);
                }

                FileMessage.removeMessagesWithKey(warnings, optionId);
            }
            else if (optionId.startsWith(KEYED_COMM_RECORD_ID)
                     || optionId.startsWith(GENERIC_COMM_RECORD_ID))
            {
                if (value.endsWith("[]"))
                {
                    int rank = 0;
                    while (value.endsWith("[]"))
                    {
                        rank++;
                        value = value.substring(0, value.length() - 2).trim();
                    }
                    commArrayNames.add(new Pair<String, Integer>(value, rank));
                }
                else
                {
                    commRecordNames.add(value);
                }

                FileMessage.removeMessagesWithKey(warnings, optionId);
            }
            else if (KEYED_LOCK_OPT_ID.equals(optionId)
                     || GENERIC_LOCK_OPT_ID.equals(optionId))
            {
                lockOpt = Boolean.valueOf(value).booleanValue();

                FileMessage.removeMessagesWithKey(warnings, optionId);
            }
            else if (optionId.startsWith(KEYED_LOCKING_RECORD_ID)
                     || optionId.startsWith(GENERIC_LOCKING_RECORD_ID))
            {
                lockingRecordNames.add(value);

                FileMessage.removeMessagesWithKey(warnings, optionId);
            }
            else if (optionId.startsWith(KEYED_READ_ONLY_FIELD_ID)
                     || optionId.startsWith(GENERIC_READ_ONLY_FIELD_ID))
            {
                readOnlyFields.add(value);

                FileMessage.removeMessagesWithKey(warnings, optionId);
            }
            else if (KEYED_READ_ONLY_FIELD_SEP_ID.equals(optionId)
                     || GENERIC_READ_ONLY_FIELD_SEP_ID.equals(optionId))
            {
                readOnlyFieldSep = value;

                FileMessage.removeMessagesWithKey(warnings, optionId);
            }
            else if (optionId.startsWith(KEYED_READ_ONLY_INIT_ID)
                     || optionId.startsWith(GENERIC_READ_ONLY_INIT_ID))
            {
                readOnlyInits.add(value);

                FileMessage.removeMessagesWithKey(warnings, optionId);
            }
            else if (KEYED_READ_ONLY_INIT_SEP_ID.equals(optionId)
                     || GENERIC_READ_ONLY_INIT_SEP_ID.equals(optionId))
            {
                readOnlyInitSep = value;

                FileMessage.removeMessagesWithKey(warnings, optionId);
            }
            else if (optionId.startsWith(KEYED_INVISIBLE_LOC_ID)
                     || optionId.startsWith(GENERIC_INVISIBLE_LOC_ID))
            {
                invisibleLocIds.add(value);

                FileMessage.removeMessagesWithKey(warnings, optionId);
            }
            else if (optionId.startsWith(KEYED_VISIBLE_LOC_ID)
                     || optionId.startsWith(GENERIC_VISIBLE_LOC_ID))
            {
                visibleLocIds.add(value);

                FileMessage.removeMessagesWithKey(warnings, optionId);
            }
            else if (optionId.startsWith(KEYED_ATOMIC_METHOD_ID)
                     || optionId.startsWith(GENERIC_ATOMIC_METHOD_ID))
            {
                atomicMethods.add(value);

                FileMessage.removeMessagesWithKey(warnings, optionId);
            }
            else if (USE_POR_ID.equals(optionId))
            {
                usePOR = Boolean.valueOf(value).booleanValue();

                FileMessage.removeMessagesWithKey(warnings, optionId);
            }
            else if (optionId.startsWith(genericKey)
                     && !optionId.equals(genericKey))
            {
                warnings.add(FileMessage.buildMessage(
                    optionId,
                    ConfigurationMessages.UNKNOWN_OPTION,
                    new String[]
                        {
                            optionId
                        }));
            }
        }

        return new DefaultMessageStore(errors, warnings);
    }

    @Override
    public boolean backtrack()
    {
        IState state = sr.getState();
        ArrayList<ITransformationBacktrackingInfo> stack = sr
            .getBacktrackingInfos();

        vf.backward();
        sf.backward();

        try
        {
            for (ListIterator<ITransformationBacktrackingInfo> tbiIter = stack
                .listIterator(stack.size()); tbiIter.hasPrevious();)
            {
                // Peek at the transformation
                ITransformationBacktrackingInfo tbi = tbiIter.previous();

                int threadId = tbi.getTransition().first;
                Transformation transformation = tbi.getTransition().second;

                vf.setContext(state, threadId);
                sf.setContext(state, threadId);

                currentDepth--;
                sf.getNotifier().notifyCurrentDepthChanged(
                    currentDepth + 1,
                    currentDepth);

                ArrayList<IPostNextStateBacktrackingInfo> postNextStateInfos = tbi
                    .getPostNextStateBacktrackingInfos();
                ArrayList<INextStateBacktrackingInfo> nextStateInfos = tbi
                    .getNextStateBacktrackingInfos();
                ArrayList< ? extends IActionBacktrackingInfo> mainInfos = tbi
                    .getMainTransformationBacktrackingInfos();

                // Roll back search metadata actions (property automaton
                // transitions, state coalescing data, etc)
                for (ListIterator<IPostNextStateBacktrackingInfo> pnsIter = postNextStateInfos
                    .listIterator(postNextStateInfos.size()); pnsIter
                    .hasPrevious();)
                {
                    IPostNextStateBacktrackingInfo bi = pnsIter.previous();
                    pnsIter.remove();

                    bi.backtrack(state);

                    // If nondeterminism still needs to be explored, then quit
                    // rolling
                    // change back, restart from here, and exit
                    if (!bi.getSchedulingStrategyInfo().isCovered())
                    {
                        isInvisible = false;
                        stateId = tbi.getStateId();
                        seenState = false;

                        if (dynamicInvisibility)
                        {
                            if (isInFindNextInvisible)
                            {
                                invisibleMoves = -1;
                            }
                            else
                            {
                                isInvisible = tbi.isInvisible();
                                lastMovedThreadId = tbi.getTransition().first;
                                invisibleMoves = tbi.getInvisibleMoves();
                            }
                        }

                        vf.forward();
                        sf.forward();

                        doPostNextStateBookkeeping(tbi, bi);

                        currentDepth++;
                        sf.getNotifier().notifyCurrentDepthChanged(
                            currentDepth - 1,
                            currentDepth);

                        if (sr.shouldStore())
                        {
                            IStoreStateResult newState = sm.storeState(state);
                            stateId = newState.getStateId();
                            seenState = newState.isSeen();
                        }

                        return true;
                    }
                }

                // Roll back actions to set up next-state
                for (ListIterator<INextStateBacktrackingInfo> nsIter = nextStateInfos
                    .listIterator(nextStateInfos.size()); nsIter.hasPrevious();)
                {
                    nsIter.previous().backtrack(state);
                    nsIter.remove();
                }

                // Roll back main transformation body actions
                for (ListIterator< ? extends IActionBacktrackingInfo> mainIter = mainInfos
                    .listIterator(mainInfos.size()); mainIter.hasPrevious();)
                {
                    IActionBacktrackingInfo bi = mainIter.previous();
                    mainIter.remove();

                    bi.backtrack(state);

                    // Remove accumulated lock accesses from forward direction
                    if (bi.getNode() instanceof AssignAction)
                    {
                        AssignAction aa = (AssignAction) bi.getNode();
                        Exp exp = aa.getExp();

                        if (exp instanceof NewRecordExp
                            || exp instanceof NewArrayExp)
                        {
                            IValue newValue = null;

                            if (bi instanceof IGlobalBacktrackingInfo)
                            {
                                int gIndex = ((IGlobalBacktrackingInfo) bi)
                                    .getGlobalIndex();
                                newValue = state.getGlobalValue(gIndex);
                            }
                            else if (bi instanceof IFieldBacktrackingInfo)
                            {
                                int fIndex = ((IFieldBacktrackingInfo) bi)
                                    .getFieldIndex();
                                IRecordValue v = ((IFieldBacktrackingInfo) bi)
                                    .getArrayOrRecordValue();

                                if (v instanceof IArrayValue)
                                {
                                    newValue = ((IArrayValue) v)
                                        .getElementValue(fIndex);
                                }
                                else
                                {
                                    newValue = v.getFieldValue(fIndex);
                                }
                            }
                            else if (bi instanceof ILocalBacktrackingInfo)
                            {
                                int lIndex = ((ILocalBacktrackingInfo) bi)
                                    .getLocalIndex();
                                int tid = threadId;
                                newValue = state.getLocalValue(tid, lIndex);
                            }

                            lockSetMap.remove(newValue);
                        }
                    }

                    if (!bi.getSchedulingStrategyInfo().isCovered())
                    {
                        stateId = tbi.getStateId();
                        seenState = false;
                        isInvisible = false;

                        if (dynamicInvisibility)
                        {
                            if (isInFindNextInvisible)
                            {
                                invisibleMoves = -1;
                            }
                            else
                            {
                                isInvisible = tbi.isInvisible();
                                lastMovedThreadId = tbi.getTransition().first;
                                invisibleMoves = tbi.getInvisibleMoves();
                            }
                        }

                        vf.forward();
                        sf.forward();

                        this.invisibleMoves = tbi.getInvisibleMoves();

                        vf.setContext(state, threadId);
                        sf.setContext(state, threadId);

                        sr.doTransition(threadId, transformation, tbi
                            .getAppropriateRestartPoint(bi), tbi);

                        return true;

                    }
                }

                //
                // All sub-parts of the transition have been rolled back
                // by now. Only nondeterminism on the selection of the overall
                // transition remains.
                //

                this.invisibleMoves = tbi.getInvisibleMoves();
                this.stateId = tbi.getStateId();
                this.lastMovedThreadId = tbi.getLastMovedThreadId();
                this.seenState = false;
                this.isInvisible = false;

                if (dynamicInvisibility)
                {
                    if (isInFindNextInvisible)
                    {
                        invisibleMoves = -1;
                    }
                    else
                    {
                        isInvisible = tbi.isInvisible();
                        lastMovedThreadId = tbi.getTransition().first;
                        invisibleMoves = tbi.getInvisibleMoves();
                    }
                }

                // Pop the transformation
                tbiIter.remove();
                tbi.backtrack(state);

                if (lastMovedThreadId != threadId)
                {
                    currentContextSwitches--;
                }

                if (!tbi.getSchedulingStrategyInfo().isCovered())
                {
                    ArrayList<Pair<Integer, Transformation>> workSet = tbi
                        .getWorkSet();
                    ArrayList<Pair<Integer, Transformation>> enabledSet = tbi
                        .getEnabledSet();

                    ISchedulingStrategyInfo ssi = tbi
                        .getSchedulingStrategyInfo();

                    int workSetIndex = ss.advise(createContext(
                        stateId,
                        invisibleMoves,
                        0,
                        state), workSet, ssi);

                    Pair<Integer, Transformation> restartTransformation = workSet
                        .get(workSetIndex);

                    int[] tids = state.getThreadIds();
                    Arrays.sort(tids);

                    int canonicalThreadIndex = Util.search(
                        tids,
                        restartTransformation.first);

                    ITransformationBacktrackingInfo newTbi;

                    if (restartTransformation.second instanceof BlockTransformation)
                    {
                        newTbi = bif.createBlockTransformationBacktrackingInfo(
                            stateId,
                            invisibleMoves,
                            isInvisible,
                            lastMovedThreadId,
                            enabledSet,
                            workSet,
                            workSet.get(workSetIndex),
                            canonicalThreadIndex,
                            ssi);
                    }
                    else
                    {
                        assert restartTransformation.second instanceof InvokeTransformation;

                        newTbi = bif
                            .createInvokeTransformationBacktrackingInfo(
                                stateId,
                                invisibleMoves,
                                isInvisible,
                                lastMovedThreadId,
                                enabledSet,
                                workSet,
                                workSet.get(workSetIndex),
                                canonicalThreadIndex,
                                ssi);
                    }

                    sr.getBacktrackingInfos().add(newTbi);

                    lastMovedThreadId = restartTransformation.first;

                    vf.forward();
                    sf.forward();
                    vf.setContext(state, restartTransformation.first);
                    sf.setContext(state, restartTransformation.first);

                    sr.doTransition(
                        restartTransformation.first,
                        restartTransformation.second,
                        null,
                        newTbi);

                    vf.removeContext();
                    sf.removeContext();

                    return true;
                }
            }

            // Okay... no transitions needing more exploration were found.
            // A null return value signifies the no restart is necessary.
            return false;
        }
        finally
        {
            vf.removeContext();
            sf.removeContext();

            vf.forward();
            sf.forward();
        }
    }

    @Override
    public IMessageStore connect(IBogorConfiguration bc)
    {
        super.connect(bc);

        IReadableIntObjectTable<Type> typeIdTypeTable = symbolTable
            .getTypeIdTypeTable();
        Map<String, RecordType> recordTable = symbolTable.getRecordTable();

        // Get a map of all the array types used
        Map<String, Map<Integer, ArrayType>> arrayTypesMap = new HashMap<String, Map<Integer, ArrayType>>();

        for (int typeId : typeIdTypeTable.keys())
        {
            Type t = typeIdTypeTable.get(typeId);

            if (t instanceof ArrayType)
            {
                ArrayType at = (ArrayType) t;

                String baseTypeName = at.getBaseType().toString().trim();

                if (!arrayTypesMap.containsKey(baseTypeName))
                {
                    arrayTypesMap.put(
                        baseTypeName,
                        new HashMap<Integer, ArrayType>());
                }

                arrayTypesMap.get(baseTypeName).put(at.getRank(), at);
            }
        }

        unshRecordTypeIds = new IntSet();
        commRecordTypeIds = new IntSet();
        lockingRecordTypeIds = new IntSet();
        readOnlyFieldTable = new IntObjectTable<IntSet>();
        readOnlyInitTable = new IntObjectTable<Set<String>>();

        visibleLocDescs = new IntSet();
        invisibleLocDescs = new IntSet();

        ArrayList<FileMessage> errors = new ArrayList<FileMessage>();
        ArrayList<FileMessage> warnings = new ArrayList<FileMessage>();

        for (String recordName : lockingRecordNames)
        {
            if (!recordTable.containsKey(recordName))
            {
                warnings.add(FileMessage.buildMessage(
                    "Invalid record type name '" + recordName + "'",
                    new String[0]));

                continue;
            }

            Type type = recordTable.get(recordName);
            lockingRecordTypeIds.add(type.getTypeId());
        }

        for (String recordName : unshRecordNames)
        {
            if (!recordTable.containsKey(recordName))
            {
                warnings.add(FileMessage.buildMessage(
                    "Invalid record type name '" + recordName + "'",
                    new String[0]));

                continue;
            }

            Type type = recordTable.get(recordName);
            unshRecordTypeIds.add(type.getTypeId());
        }

        for (Pair<String, Integer> arrayName : unshArrayNames)
        {
            StringBuilder externalName = new StringBuilder(arrayName.first);
            for (int i = 0; i < arrayName.second; i++)
            {
                externalName.append("[]");
            }
            FileMessage warningMessage = FileMessage.buildMessage(
                "Array type \"{0}\" not found in model",
                new String[]
                    {
                        externalName.toString()
                    });

            if (!arrayTypesMap.containsKey(arrayName.first))
            {
                warnings.add(warningMessage);
            }
            else if (!arrayTypesMap.get(arrayName.first).containsKey(
                arrayName.second))
            {
                warnings.add(warningMessage);
            }
            else
            {
                unshRecordTypeIds.add(arrayTypesMap.get(arrayName.first).get(
                    arrayName.second).getTypeId());
            }
        }

        for (String recordName : commRecordNames)
        {
            if (!recordTable.containsKey(recordName))
            {
                warnings.add(FileMessage.buildMessage(
                    "Invalid record type name '" + recordName + "'",
                    new String[0]));

                continue;
            }

            Type type = recordTable.get(recordName);
            commRecordTypeIds.add(type.getTypeId());
        }

        for (Pair<String, Integer> arrayName : commArrayNames)
        {
            StringBuilder externalName = new StringBuilder(arrayName.first);
            for (int i = 0; i < arrayName.second; i++)
            {
                externalName.append("[]");
            }
            FileMessage warningMessage = FileMessage.buildMessage(
                "Array type \"{0}\" not found in model",
                new String[]
                    {
                        externalName.toString()
                    });

            if (!arrayTypesMap.containsKey(arrayName.first))
            {
                warnings.add(warningMessage);
            }
            else if (!arrayTypesMap.get(arrayName.first).containsKey(
                arrayName.second))
            {
                warnings.add(warningMessage);
            }
            else
            {
                commRecordTypeIds.add(arrayTypesMap.get(arrayName.first).get(
                    arrayName.second).getTypeId());
            }
        }

        Map<String, FSMSymbolTable> functionTable = symbolTable
            .getFunctionTable();

        for (String initMap : readOnlyInits)
        {
            StringTokenizer st = new StringTokenizer(initMap, readOnlyInitSep);
            HashSet<String> fsmNames = new HashSet<String>();

            String recordName = st.hasMoreTokens() ? st.nextToken() : null;

            while (st.hasMoreTokens())
            {
                String fsmName = st.nextToken();

                if (functionTable.containsKey(fsmName))
                {
                    fsmNames.add(fsmName);
                }
                else
                {
                    warnings.add(FileMessage.buildMessage(
                        "Invalid FSM name '" + fsmName + "'",
                        new String[0]));
                }
            }

            if ((recordName == null) || (fsmNames.size() == 0))
            {
                warnings.add(FileMessage.buildMessage(
                    "Invalid init map '" + initMap + "'",
                    new String[0]));

                continue;
            }

            if (!recordTable.containsKey(recordName))
            {
                warnings.add(FileMessage.buildMessage(
                    "Invalid record type name '" + recordName + "'",
                    new String[0]));

                continue;
            }

            RecordType type = recordTable.get(recordName);
            Set<String> s = readOnlyInitTable.get(type.getTypeId());

            if (s == null)
            {
                readOnlyInitTable.put(type.getTypeId(), fsmNames);
            }
            else
            {
                s.addAll(fsmNames);
            }
        }

        for (String fieldQualifiedName : readOnlyFields)
        {
            StringTokenizer st = new StringTokenizer(
                fieldQualifiedName,
                readOnlyFieldSep);
            String recordName = st.hasMoreTokens() ? st.nextToken() : null;
            String fieldName = st.hasMoreTokens() ? st.nextToken() : null;

            if ((recordName == null) || (fieldName == null))
            {
                warnings.add(FileMessage
                    .buildMessage("Invalid field qualified name '"
                                  + fieldQualifiedName + "'", new String[0]));

                continue;
            }

            if (!recordTable.containsKey(recordName))
            {
                warnings.add(FileMessage.buildMessage(
                    "Invalid record type name '" + recordName + "'",
                    new String[0]));

                continue;
            }

            RecordType type = recordTable.get(recordName);

            if (!readOnlyInitTable.containsKey(type.getTypeId()))
            {
                warnings.add(FileMessage.buildMessage(
                    "Init FSMs unspecified for record type name '" + recordName
                            + "'",
                    new String[0]));

                continue;
            }

            if (!type.hasField(fieldName))
            {
                warnings.add(FileMessage
                    .buildMessage("Invalid field qualified name '"
                                  + fieldQualifiedName + "'", new String[0]));

                continue;
            }

            int typeId = type.getTypeId();
            int fieldIndex = type.getFieldIndex(fieldName);
            IntSet fieldIndices = readOnlyFieldTable.get(typeId);

            if (fieldIndices == null)
            {
                fieldIndices = new IntSet();
                readOnlyFieldTable.put(typeId, fieldIndices);
            }

            fieldIndices.add(fieldIndex);
        }

        ObjectIntTable<String> qLocIdLocDescTable = symbolTable
            .getQLocIdLocDescTable();

        for (String locId : invisibleLocIds)
        {
            if (qLocIdLocDescTable.containsKey(locId))
            {
                invisibleLocDescs.add(qLocIdLocDescTable.get(locId));
            }
            else
            {
                warnings.add(FileMessage.buildMessage(
                    "Invalid invisible loc id '" + locId + "'",
                    new String[0]));
            }
        }

        for (Iterator i = visibleLocIds.iterator(); i.hasNext();)
        {
            String locId = (String) i.next();

            if (qLocIdLocDescTable.containsKey(locId))
            {
                visibleLocDescs.add(qLocIdLocDescTable.get(locId));
            }
            else
            {
                warnings.add(FileMessage.buildMessage(
                    "Invalid visible loc id '" + locId + "'",
                    new String[0]));
            }
        }

        lockingRecordNames.clear();
        lockingRecordNames = null;
        unshRecordNames.clear();
        unshRecordNames = null;
        commRecordNames.clear();
        commRecordNames = null;
        commArrayNames.clear();
        commArrayNames = null;
        readOnlyFields.clear();
        readOnlyFields = null;
        readOnlyInits.clear();
        readOnlyInits = null;

        // invisibleLocs.clear();
        // invisibleLocs = null;
        // visibleLocs.clear();
        // visibleLocs = null;
        violatingLDTypeIds = new IntSet();
        lockSetMap = new HashMap<IValue, Set<ILockValue>>();

        ObjectIntTable<String> globalIndexTable = bc
            .getSymbolTable()
            .getGlobalIndexTable();

        if (globalIndexTable.containsKey(GLOBAL_ISI))
        {
            globalISIIndex = bc.getSymbolTable().getGlobalIndexTable().get(
                GLOBAL_ISI);
        }
        else
        {
            globalISIIndex = -1;
        }

        Map<String, FSM> funcDefTable = symbolTable.getFunctionDefTable();

        for (String atomicMethod : atomicMethods)
        {
            if (!funcDefTable.containsKey(atomicMethod))
            {
                warnings.add(FileMessage.buildMessage(
                    "Invalid atomic method id '" + atomicMethod + "'",
                    new String[0]));
            }
        }

        // Pre-calculate the offset at which the private locks exist on
        // record-based types. If the method call can't match each heap datatype
        // to a single "lock" field, then it inserts an appropriate error into
        // the collection passed down.
        typeIdToPrivateLockIndexMap = JavaConfigUtils
            .createTypeIdToPrivateLockIndexMap(symbolTable, errors, warnings);

        return new DefaultMessageStore(errors, warnings);
    }

    @Override
    public void doTransition(
        int threadId,
        Transformation t,
        Action a,
        ITransformationBacktrackingInfo container)
    {
        // check read only
        int[] locationStack = state.getLocationStack(threadId);
        int[] threadIds = state.getThreadIds();

        Map<IRecordValue, IntSet> writtenFieldsTable = new HashMap<IRecordValue, IntSet>();
        at.setWrittenFieldsTable(writtenFieldsTable);

        super.doTransition(threadId, t, a, container);

        at.setWrittenFieldsTable(null);

        IRecordValue[] values;
        {
            Set<IRecordValue> keySet = writtenFieldsTable.keySet();
            values = keySet.toArray(new IRecordValue[keySet.size()]);
        }

        for (int i = values.length - 1; i >= 0; i--)
        {
            final IValue v = values[i];
            int typeId = v.getTypeId();
            int[] writtenFieldIndices = writtenFieldsTable.get(v).toArray();
            IntSet fieldIndices = readOnlyFieldTable.get(typeId);

            if (fieldIndices == null)
            {
                continue;
            }

            boolean atLeastOneReadOnlyFieldWritten = false;

            for (int j = writtenFieldIndices.length - 1; j >= 0; j--)
            {
                if (fieldIndices.contains(writtenFieldIndices[j]))
                {
                    atLeastOneReadOnlyFieldWritten = true;

                    break;
                }
            }

            if ((fieldIndices == null) || !atLeastOneReadOnlyFieldWritten)
            {
                continue;
            }

            ValueVisitor vv = new ValueVisitor(new IValueVisitorAction()
                {
                    public boolean foundValue(
                        Set<IValue> seen,
                        List<IValue> workList,
                        IValue value)
                    {
                        if (value == v)
                        {
                            throw new FoundValueException();
                        }

                        return true;
                    }

                    public boolean filterType(Type t)
                    {
                        return t instanceof PrimitiveType
                               && !(t instanceof PrimitiveExtType);
                    }
                }, true);

            boolean threadLocal = true;
            boolean foundInit = false;
            final int[] otherThreadIds = new int[threadIds.length - 1];

            for (int j = threadIds.length - 1, k = 0; j >= 0; j--)
            {
                if (threadIds[j] != threadId)
                {
                    otherThreadIds[k++] = threadIds[j];
                }
            }

            for (int j = locationStack.length - 1; j >= 0; j--)
            {
                int locDesc = locationStack[j];
                String fsmId = getFSMSymbolTable(locDesc).getFSM().getId();

                Set<String> s = readOnlyInitTable.get(typeId);

                if ((s != null) && s.contains(fsmId))
                {
                    foundInit = true;

                    int enabledOtherThreads = ss.getEnabledTransformations(
                        new IEnabledTransformationsContext()
                            {
                                public IState getState()
                                {
                                    return state;
                                }

                                public int[] getThreadIds()
                                {
                                    return otherThreadIds;
                                }
                            }).size();

                    for (int k = threadIds.length - 1; (k >= 0)
                                                       && (enabledOtherThreads > 0); k--)
                    {
                        int threadId2 = threadIds[k];

                        if (threadId2 != threadId)
                        {
                            if (!isNotReachableFromThread(threadId2, vv))
                            {
                                threadLocal = false;

                                break;
                            }
                        }
                    }
                }
            }

            if (!threadLocal || !foundInit)
            {
                pw
                    .println("Unsafe! False read-only assumption on record type: "
                             + symbolTable.getTypeIdTypeTable().get(typeId)
                             + " in:");
                pw.println(t.getParent().getParent().getId() + "."
                           + t.getParent().getId());
                pw.flush();
            }

            vv.dispose();
        }
    }

    protected Set<ILockValue> getAllHeldLocks(final int threadId)
    {
        final HashSet<ILockValue> set = new HashSet<ILockValue>();
        StateValueVisitor svv = new StateValueVisitor(
            symbolTable,
            new IValueVisitorAction()
                {
                    public boolean foundValue(
                        Set<IValue> seen,
                        List<IValue> workList,
                        IValue value)
                    {
                        if (value instanceof ILockValue)
                        {
                            ILockValue lv = (ILockValue) value;

                            if (lv.getOwner() == threadId)
                            {
                                set.add(lv);
                            }
                        }

                        return true;
                    }

                    public boolean filterType(Type t)
                    {
                        return t instanceof PrimitiveType
                               && !(t instanceof PrimitiveExtType);
                    }
                },
            StateValueVisitor.DEPTH_FIRST,
            StateValueVisitor.FOLLOW_TRANSIENTS);
        svv.visit(state, null);

        return set;
    }

    @Override
    protected void findNextInvisible()
    {
        boolean olIsInFindNextInvisible = isInFindNextInvisible;
        int oldInvisibleMoves = invisibleMoves;

        try
        {
            ss.enterSimulation();
            isInFindNextInvisible = true;

            findNextInvisibleWorker();
        }
        finally
        {
            isInFindNextInvisible = olIsInFindNextInvisible;
            invisibleMoves = oldInvisibleMoves;
            ss.exitSimulation();
        }
    }

    private void findNextInvisibleWorker()
    {
        if (isInvisible || !usePOR)
        {
            return;
        }

        final int[] threadIds = state.getThreadIds();
        int size = threadIds.length;
        Arrays.sort(threadIds);

        findOneEnabledThreadNotVisible(threadIds);

        if (isInvisible)
        {
            return;
        }

        ArrayList<ITransformationBacktrackingInfo> oldBacktrackingInfos = backtrackingInfos2;
        backtrackingInfos2 = new ArrayList<ITransformationBacktrackingInfo>();

        int startIndex = Util.search(threadIds, lastMovedThreadId);
        startIndex = (startIndex >= 0) ? startIndex : 0;

        /*
         * Indicates whether the currently explored thread has yet been proven
         * (either by detection or static annotation) independent. "True" value
         * means that the thread is not yet known to be independent (more tests
         * may be done to try to infer a "false" value). "False" value means
         * that we know for certain it's independent.
         */
        boolean lastCheckedThreadPossiblyDependent = true;

        /*
         * If not -1, then the ID of a thread for which all enabled transitions
         * are independent.
         */
        int lastTestedThreadId = -1;

        boolean hasLoopInfo = loopBackpointDescs.size() > 0;
        int origStateId = stateId;

        for (int i = 0; (i < size) && lastCheckedThreadPossiblyDependent; i++)
        {
            final int threadId = threadIds[(startIndex + i) % size];
            IntSet accessedGlobals = new IntSet();
            HashSet<IValue> accessedValues = new HashSet<IValue>();
            Map<IRecordValue, IntSet> accessedFieldsTable = new HashMap<IRecordValue, IntSet>();

            ee.setReadValueSet(accessedValues);
            ee.setReadGlobalSet(accessedGlobals);
            ee.setReadFieldsTable(accessedFieldsTable);
            at.setWrittenValueSet(accessedValues);
            at.setWrittenGlobalSet(accessedGlobals);
            at.setWrittenFieldsTable(accessedFieldsTable);

            if (accessedGlobals.size() != 0)
            {
                accessedGlobals.clear();
                accessedValues.clear();
                accessedFieldsTable.clear();
                accessedFieldsTable.clear();

                continue;
            }

            Location l = getLocation(state, threadId);

            if (invisibleLocIds.contains(l.getParent().getId() + "."
                                         + l.getId()))
            {
                lastCheckedThreadPossiblyDependent = false;
                lastTestedThreadId = threadId;
            }

            boolean isC3Violated = false;

            boolean allTransformationsFromThreadAnnotatedIndependent = true;

            for (int j = l.getTransformationCount() - 1; (j >= 0)
                                                         && lastCheckedThreadPossiblyDependent; j--)
            {
                Transformation t = l.getTransformation(j);
                Pair<Integer, Transformation> transition = new Pair<Integer, Transformation>(
                    threadId,
                    t);
                ArrayList<Pair<Integer, Transformation>> enabledSet = new ArrayList<Pair<Integer, Transformation>>(
                    1);
                enabledSet.add(transition);

                int[] sortedTids = state.getThreadIds();
                Arrays.sort(sortedTids);

                // Put a container for the new transition on the main
                // backtracking stack
                ITransformationBacktrackingInfo container;

                if (t instanceof BlockTransformation)
                {
                    container = bif.createBlockTransformationBacktrackingInfo(
                        stateId,
                        invisibleMoves,
                        false,
                        lastMovedThreadId,
                        enabledSet,
                        enabledSet,
                        transition,
                        Util.search(sortedTids, threadId),
                        ss.newStrategyInfo());
                }
                else
                {
                    assert t instanceof InvokeTransformation;

                    container = bif.createInvokeTransformationBacktrackingInfo(
                        stateId,
                        invisibleMoves,
                        false,
                        lastMovedThreadId,
                        enabledSet,
                        enabledSet,
                        transition,
                        Util.search(sortedTids, threadId),
                        ss.newStrategyInfo());
                }

                backtrackingInfos2.add(container);

                allTransformationsFromThreadAnnotatedIndependent &= t
                    .getDependency() == Dependency.INDEPENDENT;

                ISchedulingStrategyContext ssc = createContext(
                    -1,
                    -1,
                    threadId,
                    state);

                doTransition(ssc, t, null, false, container);

                // Don't need to collect variables accessed for later
                // intersection
                // with full heap if we're already hinted that transition is
                // independent
                if (t.getDependency() != Dependency.INDEPENDENT)
                {
                    collectModifiedValues(
                        accessedValues,
                        accessedGlobals,
                        container.getMainTransformationBacktrackingInfos());
                }

                if (hasLoopInfo && !isC3Violated
                    && state.isThreadAlive(threadId))
                {
                    if (loopBackpointDescs
                        .contains(state.getLocation(threadId)))
                    {
                        IStoreStateResult ssr = sm.hasState(state);

                        if (ssr.isSeen())
                        {
                            if ((ssr.getStateId() == origStateId)
                                || isAmpleCycle(
                                    ssr.getStateId(),
                                    oldBacktrackingInfos))
                            {
                                isC3Violated = true;
                            }
                        }
                    }
                }

                while (backtrack())
                {
                    // Don't need to collect variables accessed for later
                    // intersection with full heap if we're already hinted that
                    // transition is independent
                    if (t.getDependency() != Dependency.INDEPENDENT)
                    {
                        collectModifiedValues(
                            accessedValues,
                            accessedGlobals,
                            container.getMainTransformationBacktrackingInfos());
                    }

                    if (hasLoopInfo && !isC3Violated
                        && state.isThreadAlive(threadId))
                    {
                        if (loopBackpointDescs.contains(state
                            .getLocation(threadId)))
                        {
                            IStoreStateResult ssr = sm.hasState(state);

                            if (ssr.isSeen())
                            {
                                if ((ssr.getStateId() == origStateId)
                                    || isAmpleCycle(
                                        ssr.getStateId(),
                                        oldBacktrackingInfos))
                                {
                                    isC3Violated = true;
                                }
                            }
                        }
                    }
                }

                if (isC3Violated || (accessedGlobals.size() != 0))
                {
                    break;
                }
            } // end of per-transformation loop

            accessedGlobals.remove(globalISIIndex);

            if (isC3Violated || (accessedGlobals.size() != 0))
            {
                accessedGlobals.clear();
                accessedValues.clear();
                accessedFieldsTable.clear();

                continue;
            }

            if (allTransformationsFromThreadAnnotatedIndependent)
            {
                // We know a priori that the transitions are all independent.
                // Tripping this flag also short-circuits all the locking-based
                // reductions below.
                lastCheckedThreadPossiblyDependent = false;
                lastTestedThreadId = threadId;
            }

            IValue[] values = accessedValues.toArray(new IValue[accessedValues
                .size()]);
            Set<IValue> protectedValues = new HashSet<IValue>();

            if (lastCheckedThreadPossiblyDependent)
            {
                // remove read only fields
                for (int j = values.length - 1; j >= 0; j--)
                {
                    IValue v = values[j];

                    if (v instanceof IArrayValue
                        && accessedFieldsTable.containsKey(v))
                    {
                        IntSet accessedfieldIndices = accessedFieldsTable
                            .get(v);

                        if ((accessedfieldIndices.size() == 1)
                            && (symbolTable.getArrayFieldIndex("length") == accessedfieldIndices
                                .toArray()[0]))
                        {
                            protectedValues.add(v);
                        }

                        continue;
                    }
                    else if (!(v instanceof IRecordValue))
                    {
                        continue;
                    }

                    if (!accessedFieldsTable.containsKey(v))
                    {
                        continue;
                    }

                    int typeId = v.getTypeId();
                    IntSet fieldIndices = readOnlyFieldTable.get(typeId);

                    if (fieldIndices == null)
                    {
                        continue;
                    }

                    int[] accessedFieldIndices = accessedFieldsTable
                        .get(v)
                        .toArray();

                    if (!fieldIndices.containsAll(accessedFieldIndices))
                    {
                        continue;
                    }

                    protectedValues.add(v);
                }

                // check if all accessed self-locking objects by t are locked by
                // t if not, then the objects are checked whether they are
                // thread-local if not, then warn the user
                for (int j = values.length - 1; j >= 0; j--)
                {
                    IValue v = values[j];

                    if (protectedValues.contains(v))
                    {
                        continue;
                    }

                    if (v instanceof IRecordValue)
                    {
                        final IRecordValue rv = (IRecordValue) v;
                        int typeId = rv.getTypeId();

                        if (lockingRecordTypeIds.contains(typeId))
                        {
                            // This cast always succeeds because we verified
                            // ahead-of-time that this field offset is mapped to
                            // a "lock" variable. In the worse case, the value
                            // is INullValue.
                            INonPrimitiveValue lv = (INonPrimitiveValue) rv
                                .getFieldValue(typeIdToPrivateLockIndexMap
                                    .get(typeId));

                            protectedValues.add(rv);

                            if (!(lv instanceof ILockValue)
                                || ((ILockValue) lv).getOwner() != threadId)
                            {
                                ValueVisitor vv = new ValueVisitor(
                                    new IValueVisitorAction()
                                        {
                                            public boolean foundValue(
                                                Set<IValue> seen,
                                                List<IValue> workList,
                                                IValue value)
                                            {
                                                if (value == rv)
                                                {
                                                    throw new FoundValueException();
                                                }

                                                return true;
                                            }

                                            public boolean filterType(Type t)
                                            {
                                                return t instanceof PrimitiveType
                                                       && !(t instanceof PrimitiveExtType);
                                            }
                                        },
                                    true);

                                for (int k = 0; k < size; k++)
                                {
                                    int threadId2 = threadIds[k];

                                    if (threadId2 != threadId)
                                    {
                                        if (!isNotReachableFromThread(
                                            threadId2,
                                            vv))
                                        {
                                            if (!atomicMethods.contains(l
                                                .getParent()
                                                .getId()))
                                            {
                                                StringWriter sw = new StringWriter();
                                                PrintWriter pw = new PrintWriter(
                                                    sw);
                                                pw
                                                    .println("Unsafe! False locking assumption on record type: "
                                                             + symbolTable
                                                                 .getTypeIdTypeTable()
                                                                 .get(typeId)
                                                             + " in:");
                                                pw.println(l
                                                    .getParent()
                                                    .getId()
                                                           + "." + l.getId());
                                                pw.flush();

                                                String s = sw.toString();
                                                pw.close();

                                                if (!warnings.contains(s))
                                                {
                                                    warnings.add(s);
                                                    this.pw.print(s);
                                                    this.pw.flush();
                                                }
                                            }
                                        }
                                    }
                                }

                                vv.dispose();
                            }
                        }
                    }
                    else if (v instanceof ILockValue && lockOpt)
                    {
                        if (((ILockValue) v).getOwner() == threadId)
                        {
                            // accessedValues.remove(v);
                            protectedValues.add(v);
                        }
                    }
                }

                // collect all non-primitive values that are "protected" by
                // self locking objects that are locked by t
                if (accessedValues.size() > 0)
                {
                    StateValueVisitor svv = new StateValueVisitor(
                        symbolTable,
                        new IValueVisitorAction()
                            {
                                public boolean foundValue(
                                    Set<IValue> seen,
                                    List<IValue> workList,
                                    IValue value)
                                {
                                    if (value instanceof IRecordValue)
                                    {
                                        IRecordValue rv = (IRecordValue) value;
                                        int typeId = rv.getTypeId();

                                        // This cast always succeeds because we
                                        // verified ahead-of-time that this
                                        // field offset is mapped toa "lock"
                                        // variable. In the worse case, the
                                        // value is INullValue.
                                        INonPrimitiveValue lv = (INonPrimitiveValue) rv
                                            .getFieldValue(typeIdToPrivateLockIndexMap
                                                .get(typeId));

                                        if (lockingRecordTypeIds
                                            .contains(typeId)
                                            && lv instanceof ILockValue
                                            && ((ILockValue) lv).getOwner() == threadId)
                                        {
                                            if (!lockOpt)
                                            {
                                                seen.add(lv);
                                            }

                                            return false;
                                        }
                                    }

                                    return true;
                                }

                                public boolean filterType(Type t)
                                {
                                    return t instanceof PrimitiveType
                                           && !(t instanceof PrimitiveExtType);
                                }
                            },
                        StateValueVisitor.DEPTH_FIRST,
                        StateValueVisitor.FOLLOW_TRANSIENTS);

                    IntIntTable threadOrderMap = new IntIntTable();

                    for (int j = 0, k = 0; j < size; j++)
                    {
                        int threadId2 = threadIds[j];

                        if (threadId2 != threadId)
                        {
                            threadOrderMap.put(threadId2, k);
                            k++;
                        }
                    }

                    svv.visit(state, threadOrderMap);

                    Set<IValue> seen = svv.getSeenSet();

                    // accessedValues.retainAll(seen);
                    for (IValue accessedValue : accessedValues)
                    {
                        if (!seen.contains(accessedValue))
                        {
                            protectedValues.add(accessedValue);
                        }
                    }

                    seen.clear();
                    svv.dispose();
                }

                if (protectedValues.size() > 0)
                {
                    if (protectedValues.containsAll(accessedValues))
                    {
                        accessedValues.clear();
                    }
                }

                if (accessedValues.isEmpty())
                {
                    lastCheckedThreadPossiblyDependent = false;
                    lastTestedThreadId = threadId;
                }

                protectedValues.clear();
            }

            // use LD
            if (lastCheckedThreadPossiblyDependent)
            {
                for (int j = 0; j < values.length; j++)
                {
                    IValue v = values[j];
                    int typeId = v.getTypeId();

                    if (unshRecordTypeIds.contains(typeId))
                    {
                        // accessedValues.remove(v);
                        protectedValues.add(v);

                        continue;
                    }
                    else if (v instanceof ILockValue
                             && (((ILockValue) v).getOwner() == threadId)
                             && lockOpt)
                    {
                        // accessedValues.remove(v);
                        protectedValues.add(v);

                        continue;
                    }
                    else if (commRecordTypeIds.contains(typeId)
                             || !(v instanceof IRecordValue))
                    {
                        continue;
                    }

                    // accessedValues.remove(v);
                    protectedValues.add(v);

                    Set<ILockValue> heldLocks = getAllHeldLocks(threadId);
                    Set<ILockValue> oldLocks = new HashSet<ILockValue>();

                    if (!intersectIfNotEmptyOrNew(v, heldLocks, oldLocks))
                    {
                        if (!violatingLDTypeIds.contains(typeId))
                        {
                            int[] locs = state.getLocationStack(threadId);
                            String[] locLocIds = symbolTable
                                .getLocDescLocIdTable();
                            String fsmId = getFSMSymbolTable(
                                locs[locs.length - 1]).getFSM().getId();

                            if (!atomicMethods.contains(fsmId))
                            {
                                StringWriter sw = new StringWriter();
                                PrintWriter pw = new PrintWriter(sw);
                                pw
                                    .println("*** LD violated by object of type: "
                                             + symbolTable
                                                 .getTypeIdTypeTable()
                                                 .get(typeId) + "***");
                                pw.println("Previous lock-set: " + oldLocks);
                                pw.println("Current lock-set: " + heldLocks);

                                for (int k = locs.length - 1; k >= 0; k--)
                                {
                                    int locDesc = locs[k];
                                    String locId = locLocIds[locDesc];
                                    FSMSymbolTable fst = getFSMSymbolTable(locDesc);
                                    Location loc = (Location) fst
                                        .getLocationDefTable()
                                        .get(locId);
                                    LocationInfo li = loc.getLocationInfo();
                                    pw.println("FSM " + loc.getParent().getId()
                                               + " at line " + li.getLine1()
                                               + ", column " + li.getColumn1());
                                    pw.println(loc);
                                }

                                pw.println();
                                pw.flush();

                                String s = sw.toString();
                                pw.close();

                                if (!warnings.contains(s))
                                {
                                    warnings.add(s);
                                    violatingLDTypeIds.add(typeId);
                                    this.pw.print(s);
                                    this.pw.flush();
                                }
                            }
                        }
                    }
                }

                if (protectedValues.size() > 0)
                {
                    if (protectedValues.containsAll(accessedValues))
                    {
                        accessedValues.clear();
                    }
                }

                lastCheckedThreadPossiblyDependent = accessedValues.size() > 0;

                if (!lastCheckedThreadPossiblyDependent)
                {
                    lastTestedThreadId = threadId;
                }

                protectedValues.clear();
            }

            accessedGlobals.clear();
            accessedValues.clear();
            accessedFieldsTable.clear();
        }

        ee.setReadValueSet(null);
        ee.setReadGlobalSet(null);
        at.setWrittenValueSet(null);
        at.setWrittenGlobalSet(null);

        if (!lastCheckedThreadPossiblyDependent)
        {
            lastMovedThreadId = lastTestedThreadId;
            isInvisible = true;
        }

        backtrackingInfos2 = oldBacktrackingInfos;
    }

    protected boolean intersectIfNotEmptyOrNew(
        IValue v,
        Set<ILockValue> lockSet,
        Set<ILockValue> oldLockSet)
    {
        if (lockSetMap.get(v) == null)
        {
            lockSetMap.put(v, lockSet);

            return true;
        }

        Set<ILockValue> temp = lockSetMap.get(v);

        oldLockSet.addAll(temp);

        temp.retainAll(lockSet);

        if (temp.isEmpty())
        {
            return false;
        }
        else
        {
            return true;
        }
    }
}
